T:Type, eq:EqDecider(T), ll:(T List) List, x:T.
(x  l-union-list(eq;ll))  (l:T List. (l  ll) & (x  l)) 

latex

Definitions

(x  l), type List, P & Q, x:A. B(x), P  Q, l-union(eq;as;bs), list_accum(x,a.f(x;a);y;l), P  Q, x:A. B(x), EqDecider(T), Type, t  T, x:AB(x), x:AB(x), left+right, False, P  Q, nil, Prop, {T}, P  Q, car.cdr, x,y. t(x;y), x.A(x), x. t(x), , a<b, s = t, A & B, True, T, l-union-list(eq;ll), tl(l), n-m, if a<b c ; d fi, i<j, b, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), Y, ||as||, A, AB, , {x:A| B(x) }

Lemmas

l-union-list wf, squash wf, true wf, member-union, or functionality wrt iff, exists functionality wrt iff, and functionality wrt iff, cons member, all functionality wrt iff, iff functionality wrt iff, iff wf, list accum wf, l-union wf, l member wf, nil member, deq wf